$\forall$$i$:Id, $X$:Type, $p$:FinProbSpace, $x_{0}$:$X$, $P$:($X$$\rightarrow\mathbb{B}$).
\\[0ex]Normal($X$) $\Rightarrow$ $\vdash$${\it es}$.pre{-}init1{-}p(${\it es}$;$i$;"x";$X$;$x_{0}$;"a";$p$;$P$)